#include <stdio.h>
#include <assert.h>
#include <stdlib.h>
#include <time.h>
#include "verific.h"
#include "lista.h"

struct slista {
elem *a;
int n;
};

lista
lista_create(const int ne)
{
  lista res;
  assert(ne>=0);/* PRE: { ne>=0 } */
  res=(lista)malloc(sizeof(struct slista));
  res->a=(elem *)malloc(ne*sizeof(elem));/*(*res).a=(int *)ma...*/
  if ((*res).a!=NULL)
    (*res).n=ne;
  else
    (*res).n=0;
  return res;
  /* POS: { Hay memoria ==> res.n=ne /\ created(res.a) } */
}

lista
lista_clone(const lista a)
{
  /* PRE: { a==A } */
  lista res;
  res=(struct slista *)malloc(sizeof(struct slista));
  res->a=(elem *)malloc(a->n*sizeof(elem));
  if (res->a!=NULL)
    res->n=(*a).n;
  else
    res->n=0;
  return res;
  /* POS: { Hay memoria ==> created(res.a) /\ res==a==A /\ res.n==a.n */
}

void
lista_destroy(lista a)
{
  assert((*a).a!=NULL);
  free((*a).a);
  free(a);
  a=NULL;
  assert(a==NULL);
}

/* Proyector */

int
lista_length(const lista a)
{
  assert((*a).a!=NULL);
  return a->n;
  /* POS: { a=A /\ l=length(a) } */
}

/* Procedimientos */

void
lista_swap(lista a, const int i, const int j)
{
  elem y;
  assert((*a).n>i && i>=0 && (*a).n>j && j>=0);
  y=a->a[i];
  a->a[i]=a->a[j];
  a->a[j]=y;
  /* POS: { a=swap(A,i,j) } */
}

void
lista_reverse(lista a)
{
  /* PRE: { a=A } */
  int i=0;
  while(i<((*a).n)/2)
    {
      lista_swap(a,i,((*a).n)-1-i);
      i=i+1;
    }
  /* POS: { (FORALL i: 0<= i < length(a): a[i] = A[length(A)-i-1]) /\ length(a)=length(A) } */
}

void
lista_fillStdIn(lista a)
{
  /* PRE: { a=A } */
  int i=0;
  while(i<(*a).n)
    {
      printf("Ingrese el valor del array indexado en %i\n\t",i);
      verific_elem(&((*a).a[i]));
      i=i+1;
    }
  /* POS: { llenado a por teclado /\ length(a)=length(A) } */
}

void
lista_fillRand(lista a)
{
  /* PRE: { a=A } */
  int i=0;
  time_t t;
  srand((int)time(&t));
  while(i<(a->n))
    {
      a->a[i]=1+(int)((100.0*rand())/(RAND_MAX+1.0));
      i=i+1;
    }
  /* POS: { llenado a con valores al azar /\ length(a)=length(A) } */
}

void
lista_showStdOut(const lista a)
{
  /* PRE: { a=A } */
  int i=0;
  printf("El array contien:\n\t[ ");
  while(i<(a->n))
    {
      if (i==(a->n)-1){
	printf_elem(a->a[i]);
	printf(" ]\n");
      }
      else{
	printf_elem(a->a[i]);
	printf(", ");
      }
      i=i+1;
    }
  /* POS: { a=A /\ Valores de A en pantalla } */
}

void
lista_copy(lista b, const lista a)
{
  /* PRE: { a=A /\ b=B /\ length(a) <= length(b)} */
  int i=0;
  assert(sizeof(b)==sizeof(struct slista));
  b->a=(elem *)realloc(((*b).a),(a->n)*sizeof(elem));
  if ((*b).a!=NULL)
    {
      (*b).n=(a->n);
      while(i<(*b).n)
	{
	  b->a[i]=a->a[i];
	  i=i+1;
	}
    }
  else
    (*b).n=0;
  /* POS: { a=A /\ b=a } */
}
